Nuprl Definition : constant_function
11,40
postcript
pdf
constant_function(
f
;
A
;
B
) ==
a
,
a'
:
A
.
f
(
a
) =
f
(
a'
)
latex
clarification:
constant_function(
f
;
A
;
B
) ==
a
:
A
,
a'
:
A
.
f
(
a
) =
f
(
a'
)
B
latex
Definitions
x
:
A
.
B
(
x
)
,
s
=
t
,
f
(
a
)
FDL editor aliases
constant_function
origin
a,a':A. f(a) = f(a')
a:A, a':A. f(a) = f(a') 
B a,a':A. f(a) = f(a')
a:A, a':A. f(a) = f(a') B x:A. B(x)